p:FinProbSpace, n:, X:RandomVariable(p;n). 0  X  (e:. 0 < e  E(n;e  X)  (E(n;X)/e)) 

latex

Definitions

x:A. B(x), P  Q, (r/s), P  Q, P  Q, t  T, A, , P & Q, X  Y, rv-const(a), A  B, q*X, S  T, suptype(S; T), True, if b then t else f fi , tt, ff, T, False, , , Unit, RandomVariable(p;n), Outcome,

Lemmas

qdiv wf, qless transitivity 2 qorder, qle weakening eq qorder, qless irreflexivity, expectation-rv-scale, int-rational, expectation-monotone, rv-qle wf, rv-const wf, rv-scale wf, qle wf, expectation wf, qless wf, int inc rationals, rationals wf, rv-le wf, random-variable wf, nat wf, finite-prob-space wf, not functionality wrt iff, assert wf, qeq wf2, assert-qeq, qmul wf, qinv wf, qmul assoc qrng, qmul one qrng, qmul comm qrng, qinv-positive, int seg wf, p-outcome wf, q le wf, bool wf, bnot wf, not wf, iff transitivity, eqtt to assert, assert-q le-eq, eqff to assert, assert of bnot, squash wf, true wf, qmul preserves qle, qmul-qdiv-cancel2, qmul zero qrng